Nuprl Lemma : trivial_map
11,40
postcript
pdf
T
:Type,
a
:(
T
List),
f
:(
T
T
). (
x
:
T
. (
x
a
)
(
f
(
x
) =
x
))
(map(
f
;
a
) =
a
)
latex
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Id
,
Id{
T
}
Lemmas
l
member
wf
,
map
equal2
,
tidentity
wf
,
map
id
origin
T:Type, a:(T List), f:(T
T). (x:T. (x 
a) 
(f(x) = x)) (map(f;a) = a) T:Type, a:(T List), f:(TT). (x:T. (x a) (f(x) = x)) (map(f;a) = a) 
T Qx:A. B(x)